0 CpxTRS
↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxTypedWeightedTrs
↳5 CompletionProof (UPPER BOUND(ID), 43 ms)
↳6 CpxTypedWeightedCompleteTrs
↳7 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳8 CpxRNTS
↳9 CompleteCoflocoProof (⇔, 4300 ms)
↳10 BOUNDS(1, n^3)
lessElements(l, t) → lessE(l, t, 0)
lessE(l, t, n) → if(le(length(l), n), le(length(toList(t)), n), l, t, n)
if(true, b, l, t, n) → l
if(false, true, l, t, n) → t
if(false, false, l, t, n) → lessE(l, t, s(n))
length(nil) → 0
length(cons(n, l)) → s(length(l))
toList(leaf) → nil
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2)))
append(nil, l2) → l2
append(cons(n, l1), l2) → cons(n, append(l1, l2))
le(s(n), 0) → false
le(0, m) → true
le(s(n), s(m)) → le(n, m)
a → c
a → d
lessElements(l, t) → lessE(l, t, 0) [1]
lessE(l, t, n) → if(le(length(l), n), le(length(toList(t)), n), l, t, n) [1]
if(true, b, l, t, n) → l [1]
if(false, true, l, t, n) → t [1]
if(false, false, l, t, n) → lessE(l, t, s(n)) [1]
length(nil) → 0 [1]
length(cons(n, l)) → s(length(l)) [1]
toList(leaf) → nil [1]
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2))) [1]
append(nil, l2) → l2 [1]
append(cons(n, l1), l2) → cons(n, append(l1, l2)) [1]
le(s(n), 0) → false [1]
le(0, m) → true [1]
le(s(n), s(m)) → le(n, m) [1]
a → c [1]
a → d [1]
lessElements(l, t) → lessE(l, t, 0) [1]
lessE(l, t, n) → if(le(length(l), n), le(length(toList(t)), n), l, t, n) [1]
if(true, b, l, t, n) → l [1]
if(false, true, l, t, n) → t [1]
if(false, false, l, t, n) → lessE(l, t, s(n)) [1]
length(nil) → 0 [1]
length(cons(n, l)) → s(length(l)) [1]
toList(leaf) → nil [1]
toList(node(t1, n, t2)) → append(toList(t1), cons(n, toList(t2))) [1]
append(nil, l2) → l2 [1]
append(cons(n, l1), l2) → cons(n, append(l1, l2)) [1]
le(s(n), 0) → false [1]
le(0, m) → true [1]
le(s(n), s(m)) → le(n, m) [1]
a → c [1]
a → d [1]
| lessElements :: nil:cons:leaf:node → nil:cons:leaf:node → nil:cons:leaf:node lessE :: nil:cons:leaf:node → nil:cons:leaf:node → 0:s → nil:cons:leaf:node 0 :: 0:s if :: true:false → true:false → nil:cons:leaf:node → nil:cons:leaf:node → 0:s → nil:cons:leaf:node le :: 0:s → 0:s → true:false length :: nil:cons:leaf:node → 0:s toList :: nil:cons:leaf:node → nil:cons:leaf:node true :: true:false false :: true:false s :: 0:s → 0:s nil :: nil:cons:leaf:node cons :: a → nil:cons:leaf:node → nil:cons:leaf:node leaf :: nil:cons:leaf:node node :: nil:cons:leaf:node → a → nil:cons:leaf:node → nil:cons:leaf:node append :: nil:cons:leaf:node → nil:cons:leaf:node → nil:cons:leaf:node a :: c:d c :: c:d d :: c:d |
length(v0) → null_length [0]
toList(v0) → null_toList [0]
append(v0, v1) → null_append [0]
le(v0, v1) → null_le [0]
if(v0, v1, v2, v3, v4) → null_if [0]
null_length, null_toList, null_append, null_le, null_if, const
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
0 => 0
true => 2
false => 1
nil => 1
leaf => 0
c => 0
d => 1
null_length => 0
null_toList => 0
null_append => 0
null_le => 0
null_if => 0
const => 0
a -{ 1 }→ 1 :|:
a -{ 1 }→ 0 :|:
append(z, z') -{ 1 }→ l2 :|: z = 1, z' = l2, l2 >= 0
append(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
append(z, z') -{ 1 }→ 1 + n + append(l1, l2) :|: n >= 0, z = 1 + n + l1, z' = l2, l1 >= 0, l2 >= 0
if(z, z', z'', z1, z2) -{ 1 }→ l :|: z = 2, b >= 0, n >= 0, z1 = t, z' = b, l >= 0, t >= 0, z2 = n, z'' = l
if(z, z', z'', z1, z2) -{ 1 }→ t :|: n >= 0, z' = 2, z = 1, z1 = t, l >= 0, t >= 0, z2 = n, z'' = l
if(z, z', z'', z1, z2) -{ 1 }→ lessE(l, t, 1 + n) :|: n >= 0, z = 1, z1 = t, l >= 0, t >= 0, z' = 1, z2 = n, z'' = l
if(z, z', z'', z1, z2) -{ 0 }→ 0 :|: z1 = v3, v0 >= 0, v4 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, z2 = v4, v2 >= 0, v3 >= 0
le(z, z') -{ 1 }→ le(n, m) :|: n >= 0, z' = 1 + m, z = 1 + n, m >= 0
le(z, z') -{ 1 }→ 2 :|: z' = m, z = 0, m >= 0
le(z, z') -{ 1 }→ 1 :|: n >= 0, z = 1 + n, z' = 0
le(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
length(z) -{ 1 }→ 0 :|: z = 1
length(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
length(z) -{ 1 }→ 1 + length(l) :|: z = 1 + n + l, n >= 0, l >= 0
lessE(z, z', z'') -{ 1 }→ if(le(length(l), n), le(length(toList(t)), n), l, t, n) :|: n >= 0, z' = t, z'' = n, z = l, l >= 0, t >= 0
lessElements(z, z') -{ 1 }→ lessE(l, t, 0) :|: z' = t, z = l, l >= 0, t >= 0
toList(z) -{ 1 }→ append(toList(t1), 1 + n + toList(t2)) :|: n >= 0, t1 >= 0, z = 1 + t1 + n + t2, t2 >= 0
toList(z) -{ 1 }→ 1 :|: z = 0
toList(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
| eq(start(V, V1, V4, V8, V9),0,[lessElements(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V4, V8, V9),0,[lessE(V, V1, V4, Out)],[V >= 0,V1 >= 0,V4 >= 0]). eq(start(V, V1, V4, V8, V9),0,[if(V, V1, V4, V8, V9, Out)],[V >= 0,V1 >= 0,V4 >= 0,V8 >= 0,V9 >= 0]). eq(start(V, V1, V4, V8, V9),0,[length(V, Out)],[V >= 0]). eq(start(V, V1, V4, V8, V9),0,[toList(V, Out)],[V >= 0]). eq(start(V, V1, V4, V8, V9),0,[append(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V4, V8, V9),0,[le(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V4, V8, V9),0,[a(Out)],[]). eq(lessElements(V, V1, Out),1,[lessE(V2, V3, 0, Ret)],[Out = Ret,V1 = V3,V = V2,V2 >= 0,V3 >= 0]). eq(lessE(V, V1, V4, Out),1,[length(V5, Ret00),le(Ret00, V6, Ret0),toList(V7, Ret100),length(Ret100, Ret10),le(Ret10, V6, Ret1),if(Ret0, Ret1, V5, V7, V6, Ret2)],[Out = Ret2,V6 >= 0,V1 = V7,V4 = V6,V = V5,V5 >= 0,V7 >= 0]). eq(if(V, V1, V4, V8, V9, Out),1,[],[Out = V10,V = 2,V11 >= 0,V12 >= 0,V8 = V13,V1 = V11,V10 >= 0,V13 >= 0,V9 = V12,V4 = V10]). eq(if(V, V1, V4, V8, V9, Out),1,[],[Out = V14,V15 >= 0,V1 = 2,V = 1,V8 = V14,V16 >= 0,V14 >= 0,V9 = V15,V4 = V16]). eq(if(V, V1, V4, V8, V9, Out),1,[lessE(V17, V18, 1 + V19, Ret3)],[Out = Ret3,V19 >= 0,V = 1,V8 = V18,V17 >= 0,V18 >= 0,V1 = 1,V9 = V19,V4 = V17]). eq(length(V, Out),1,[],[Out = 0,V = 1]). eq(length(V, Out),1,[length(V20, Ret11)],[Out = 1 + Ret11,V = 1 + V20 + V21,V21 >= 0,V20 >= 0]). eq(toList(V, Out),1,[],[Out = 1,V = 0]). eq(toList(V, Out),1,[toList(V22, Ret01),toList(V24, Ret111),append(Ret01, 1 + V23 + Ret111, Ret4)],[Out = Ret4,V23 >= 0,V22 >= 0,V = 1 + V22 + V23 + V24,V24 >= 0]). eq(append(V, V1, Out),1,[],[Out = V25,V = 1,V1 = V25,V25 >= 0]). eq(append(V, V1, Out),1,[append(V27, V28, Ret12)],[Out = 1 + Ret12 + V26,V26 >= 0,V = 1 + V26 + V27,V1 = V28,V27 >= 0,V28 >= 0]). eq(le(V, V1, Out),1,[],[Out = 1,V29 >= 0,V = 1 + V29,V1 = 0]). eq(le(V, V1, Out),1,[],[Out = 2,V1 = V30,V = 0,V30 >= 0]). eq(le(V, V1, Out),1,[le(V31, V32, Ret5)],[Out = Ret5,V31 >= 0,V1 = 1 + V32,V = 1 + V31,V32 >= 0]). eq(a(Out),1,[],[Out = 0]). eq(a(Out),1,[],[Out = 1]). eq(length(V, Out),0,[],[Out = 0,V33 >= 0,V = V33]). eq(toList(V, Out),0,[],[Out = 0,V34 >= 0,V = V34]). eq(append(V, V1, Out),0,[],[Out = 0,V35 >= 0,V36 >= 0,V = V35,V1 = V36]). eq(le(V, V1, Out),0,[],[Out = 0,V37 >= 0,V38 >= 0,V = V37,V1 = V38]). eq(if(V, V1, V4, V8, V9, Out),0,[],[Out = 0,V8 = V39,V40 >= 0,V41 >= 0,V4 = V42,V43 >= 0,V = V40,V1 = V43,V9 = V41,V42 >= 0,V39 >= 0]). input_output_vars(lessElements(V,V1,Out),[V,V1],[Out]). input_output_vars(lessE(V,V1,V4,Out),[V,V1,V4],[Out]). input_output_vars(if(V,V1,V4,V8,V9,Out),[V,V1,V4,V8,V9],[Out]). input_output_vars(length(V,Out),[V],[Out]). input_output_vars(toList(V,Out),[V],[Out]). input_output_vars(append(V,V1,Out),[V,V1],[Out]). input_output_vars(le(V,V1,Out),[V,V1],[Out]). input_output_vars(a(Out),[],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. non_recursive : [a/1]
1. recursive : [append/3]
2. recursive : [le/3]
3. recursive : [length/2]
4. recursive [non_tail,multiple] : [toList/2]
5. recursive : [if/6,lessE/4]
6. non_recursive : [lessElements/3]
7. non_recursive : [start/5]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into a/1
1. SCC is partially evaluated into append/3
2. SCC is partially evaluated into le/3
3. SCC is partially evaluated into length/2
4. SCC is partially evaluated into toList/2
5. SCC is partially evaluated into lessE/4
6. SCC is completely evaluated into other SCCs
7. SCC is partially evaluated into start/5
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations a/1
* CE 31 is refined into CE [32]
* CE 30 is refined into CE [33]
### Cost equations --> "Loop" of a/1
* CEs [32] --> Loop 20
* CEs [33] --> Loop 21
### Ranking functions of CR a(Out)
#### Partial ranking functions of CR a(Out)
### Specialization of cost equations append/3
* CE 25 is refined into CE [34]
* CE 23 is refined into CE [35]
* CE 24 is refined into CE [36]
### Cost equations --> "Loop" of append/3
* CEs [36] --> Loop 22
* CEs [34] --> Loop 23
* CEs [35] --> Loop 24
### Ranking functions of CR append(V,V1,Out)
* RF of phase [22]: [V]
#### Partial ranking functions of CR append(V,V1,Out)
* Partial RF of phase [22]:
- RF of loop [22:1]:
V
### Specialization of cost equations le/3
* CE 29 is refined into CE [37]
* CE 26 is refined into CE [38]
* CE 27 is refined into CE [39]
* CE 28 is refined into CE [40]
### Cost equations --> "Loop" of le/3
* CEs [40] --> Loop 25
* CEs [37] --> Loop 26
* CEs [38] --> Loop 27
* CEs [39] --> Loop 28
### Ranking functions of CR le(V,V1,Out)
* RF of phase [25]: [V,V1]
#### Partial ranking functions of CR le(V,V1,Out)
* Partial RF of phase [25]:
- RF of loop [25:1]:
V
V1
### Specialization of cost equations length/2
* CE 17 is refined into CE [41]
* CE 19 is refined into CE [42]
* CE 18 is refined into CE [43]
### Cost equations --> "Loop" of length/2
* CEs [43] --> Loop 29
* CEs [41,42] --> Loop 30
### Ranking functions of CR length(V,Out)
* RF of phase [29]: [V]
#### Partial ranking functions of CR length(V,Out)
* Partial RF of phase [29]:
- RF of loop [29:1]:
V
### Specialization of cost equations toList/2
* CE 22 is refined into CE [44]
* CE 20 is refined into CE [45]
* CE 21 is refined into CE [46,47,48,49]
### Cost equations --> "Loop" of toList/2
* CEs [49] --> Loop 31
* CEs [48] --> Loop 32
* CEs [46] --> Loop 33
* CEs [47] --> Loop 34
* CEs [44] --> Loop 35
* CEs [45] --> Loop 36
### Ranking functions of CR toList(V,Out)
* RF of phase [31,32,33,34]: [V]
#### Partial ranking functions of CR toList(V,Out)
* Partial RF of phase [31,32,33,34]:
- RF of loop [31:1,31:2,32:1,32:2,33:1,33:2,34:1,34:2]:
V
### Specialization of cost equations lessE/4
* CE 15 is refined into CE [50,51,52,53,54,55,56,57]
* CE 16 is refined into CE [58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81]
* CE 13 is refined into CE [82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152]
* CE 14 is refined into CE [153,154,155]
### Cost equations --> "Loop" of lessE/4
* CEs [155] --> Loop 37
* CEs [154] --> Loop 38
* CEs [153] --> Loop 39
* CEs [55,56,57] --> Loop 40
* CEs [51,52] --> Loop 41
* CEs [67] --> Loop 42
* CEs [112,113] --> Loop 43
* CEs [91,104,114,115,116,117,127] --> Loop 44
* CEs [58,59,60,61,62,63,64,65,66,68,69,70,71,72,73,74,75,76,77,78,79,80,81] --> Loop 45
* CEs [50,53,54,82,83,84,85,86,87,88,89,90,92,93,94,95,96,97,98,99,100,101,102,103,105,106,107,108,109,110,111,118,119,120,121,122,123,124,125,126,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152] --> Loop 46
### Ranking functions of CR lessE(V,V1,V4,Out)
* RF of phase [37]: [V-V4,V1-V4+1]
#### Partial ranking functions of CR lessE(V,V1,V4,Out)
* Partial RF of phase [37]:
- RF of loop [37:1]:
V-V4
V1-V4+1
### Specialization of cost equations start/5
* CE 2 is refined into CE [156]
* CE 3 is refined into CE [157,158,159]
* CE 4 is refined into CE [160]
* CE 5 is refined into CE [161]
* CE 6 is refined into CE [162,163,164,165,166]
* CE 7 is refined into CE [167,168,169,170,171,172]
* CE 8 is refined into CE [173,174]
* CE 9 is refined into CE [175,176,177]
* CE 10 is refined into CE [178,179,180,181]
* CE 11 is refined into CE [182,183,184,185,186]
* CE 12 is refined into CE [187,188]
### Cost equations --> "Loop" of start/5
* CEs [156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188] --> Loop 47
### Ranking functions of CR start(V,V1,V4,V8,V9)
#### Partial ranking functions of CR start(V,V1,V4,V8,V9)
Computing Bounds
=====================================
#### Cost of chains of a(Out):
* Chain [21]: 1
with precondition: [Out=0]
* Chain [20]: 1
with precondition: [Out=1]
#### Cost of chains of append(V,V1,Out):
* Chain [[22],24]: 1*it(22)+1
Such that:it(22) =< -V1+Out
with precondition: [V+V1=Out+1,V>=2,V1>=0]
* Chain [[22],23]: 1*it(22)+0
Such that:it(22) =< Out
with precondition: [V1>=0,Out>=1,V>=Out]
* Chain [24]: 1
with precondition: [V=1,V1=Out,V1>=0]
* Chain [23]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of le(V,V1,Out):
* Chain [[25],28]: 1*it(25)+1
Such that:it(25) =< V
with precondition: [Out=2,V>=1,V1>=V]
* Chain [[25],27]: 1*it(25)+1
Such that:it(25) =< V1
with precondition: [Out=1,V1>=1,V>=V1+1]
* Chain [[25],26]: 1*it(25)+0
Such that:it(25) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [28]: 1
with precondition: [V=0,Out=2,V1>=0]
* Chain [27]: 1
with precondition: [V1=0,Out=1,V>=1]
* Chain [26]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of length(V,Out):
* Chain [[29],30]: 1*it(29)+1
Such that:it(29) =< V
with precondition: [Out>=1,V>=Out]
* Chain [30]: 1
with precondition: [Out=0,V>=0]
#### Cost of chains of toList(V,Out):
* Chain [36]: 1
with precondition: [V=0,Out=1]
* Chain [35]: 0
with precondition: [Out=0,V>=0]
* Chain [multiple([31,32,33,34],[[36],[35]])]: 1*it(31)+5*it(32)+1*it([36])+1*s(6)+1*s(7)+0
Such that:aux(3) =< V
aux(4) =< V+1
aux(5) =< 2*V+1
it(32) =< aux(3)
it([36]) =< aux(4)
it(31) =< aux(5)
it(32) =< aux(5)
it([36]) =< aux(5)
aux(2) =< aux(3)-1
s(6) =< it(31)*aux(3)
s(7) =< it(32)*aux(2)
with precondition: [V>=1,Out>=0,V+1>=Out]
#### Cost of chains of lessE(V,V1,V4,Out):
* Chain [[37],46]: 6*it(37)+49*s(8)+88*s(10)+22*s(13)+125*s(25)+25*s(26)+25*s(27)+25*s(29)+25*s(30)+1*s(422)+2*s(423)+5*s(424)+1*s(425)+1*s(426)+1*s(427)+1*s(428)+1*s(429)+7
Such that:aux(58) =< 1
it(37) =< V1-V4+1
aux(62) =< 2*V1+1
aux(72) =< V
aux(73) =< V1
aux(74) =< V1+1
s(13) =< aux(58)
s(8) =< aux(72)
s(10) =< aux(74)
s(25) =< aux(73)
s(26) =< aux(74)
s(27) =< aux(62)
s(25) =< aux(62)
s(26) =< aux(62)
s(28) =< aux(73)-1
s(29) =< s(27)*aux(73)
s(30) =< s(25)*s(28)
aux(69) =< aux(73)*2+1
aux(68) =< aux(73)+1
aux(67) =< aux(73)
s(433) =< it(37)*aux(72)
s(422) =< it(37)*aux(72)
s(430) =< it(37)*aux(69)
s(431) =< it(37)*aux(68)
s(432) =< it(37)*aux(67)
s(429) =< s(431)
s(423) =< s(433)
s(424) =< s(432)
s(425) =< s(431)
s(426) =< s(430)
s(424) =< s(430)
s(425) =< s(430)
s(427) =< s(426)*aux(73)
s(428) =< s(424)*s(28)
with precondition: [Out=0,V4>=1,V>=V4+1,V1>=V4]
* Chain [[37],45]: 6*it(37)+1*s(422)+2*s(423)+5*s(424)+1*s(425)+1*s(426)+1*s(427)+1*s(428)+1*s(429)+23*s(434)+7*s(435)+50*s(444)+10*s(445)+10*s(446)+10*s(448)+10*s(449)+19*s(493)+7
Such that:aux(93) =< 1
it(37) =< V1-V4+1
aux(97) =< 2*V1+1
aux(99) =< V1
aux(100) =< V1+1
aux(101) =< Out
s(435) =< aux(93)
s(493) =< aux(101)
s(434) =< aux(100)
s(444) =< aux(99)
s(445) =< aux(100)
s(446) =< aux(97)
s(444) =< aux(97)
s(445) =< aux(97)
s(419) =< aux(99)-1
s(448) =< s(446)*aux(99)
s(449) =< s(444)*s(419)
aux(69) =< aux(99)*2+1
aux(68) =< aux(99)+1
aux(67) =< aux(99)
s(433) =< it(37)*aux(101)
s(422) =< it(37)*aux(101)
s(430) =< it(37)*aux(69)
s(431) =< it(37)*aux(68)
s(432) =< it(37)*aux(67)
s(429) =< s(431)
s(423) =< s(433)
s(424) =< s(432)
s(425) =< s(431)
s(426) =< s(430)
s(424) =< s(430)
s(425) =< s(430)
s(427) =< s(426)*aux(99)
s(428) =< s(424)*s(419)
with precondition: [V=Out,V4>=1,V>=V4+1,V1>=V4]
* Chain [[37],40]: 6*it(37)+1*s(422)+2*s(423)+5*s(424)+1*s(425)+1*s(426)+1*s(427)+1*s(428)+1*s(429)+7*s(573)+10*s(580)+2*s(581)+2*s(582)+2*s(584)+2*s(585)+1*s(597)+6
Such that:it(37) =< V-V4
aux(106) =< Out+1
aux(107) =< 2*Out+1
aux(109) =< V
aux(110) =< Out
s(573) =< aux(109)
s(580) =< aux(110)
s(581) =< aux(106)
s(582) =< aux(107)
s(580) =< aux(107)
s(581) =< aux(107)
s(419) =< aux(110)-1
s(584) =< s(582)*aux(110)
s(585) =< s(580)*s(419)
s(597) =< aux(106)
aux(69) =< aux(110)*2+1
aux(68) =< aux(110)+1
aux(67) =< aux(110)
s(433) =< it(37)*aux(109)
s(422) =< it(37)*aux(109)
s(430) =< it(37)*aux(69)
s(431) =< it(37)*aux(68)
s(432) =< it(37)*aux(67)
s(429) =< s(431)
s(423) =< s(433)
s(424) =< s(432)
s(425) =< s(431)
s(426) =< s(430)
s(424) =< s(430)
s(425) =< s(430)
s(427) =< s(426)*aux(110)
s(428) =< s(424)*s(419)
with precondition: [V1=Out,V4>=1,V>=V4+2,V1>=V4]
* Chain [46]: 49*s(8)+73*s(10)+22*s(13)+125*s(25)+25*s(26)+25*s(27)+25*s(29)+25*s(30)+15*s(50)+7
Such that:aux(58) =< 1
aux(59) =< V
aux(60) =< V1
aux(61) =< V1+1
aux(62) =< 2*V1+1
aux(63) =< V4
s(13) =< aux(58)
s(8) =< aux(59)
s(10) =< aux(63)
s(25) =< aux(60)
s(26) =< aux(61)
s(27) =< aux(62)
s(25) =< aux(62)
s(26) =< aux(62)
s(28) =< aux(60)-1
s(29) =< s(27)*aux(60)
s(30) =< s(25)*s(28)
s(50) =< aux(61)
with precondition: [Out=0,V>=0,V1>=0,V4>=0]
* Chain [45]: 17*s(434)+7*s(435)+50*s(444)+10*s(445)+10*s(446)+10*s(448)+10*s(449)+6*s(469)+19*s(493)+7
Such that:aux(93) =< 1
aux(94) =< V
aux(95) =< V1
aux(96) =< V1+1
aux(97) =< 2*V1+1
aux(98) =< V4
s(435) =< aux(93)
s(493) =< aux(94)
s(434) =< aux(98)
s(444) =< aux(95)
s(445) =< aux(96)
s(446) =< aux(97)
s(444) =< aux(97)
s(445) =< aux(97)
s(447) =< aux(95)-1
s(448) =< s(446)*aux(95)
s(449) =< s(444)*s(447)
s(469) =< aux(96)
with precondition: [V=Out,V>=0,V1>=0,V4>=0]
* Chain [44]: 35*s(602)+7*s(603)+7*s(604)+7*s(606)+7*s(607)+5*s(608)+5*s(620)+5
Such that:aux(116) =< V
aux(117) =< V1
aux(118) =< V1+1
aux(119) =< 2*V1+1
s(620) =< aux(116)
s(602) =< aux(117)
s(603) =< aux(118)
s(604) =< aux(119)
s(602) =< aux(119)
s(603) =< aux(119)
s(605) =< aux(117)-1
s(606) =< s(604)*aux(117)
s(607) =< s(602)*s(605)
s(608) =< aux(118)
with precondition: [V4=0,Out=0,V>=0,V1>=1]
* Chain [43]: 2*s(676)+5
Such that:aux(120) =< V
s(676) =< aux(120)
with precondition: [V4=0,Out=0,V>=1,V1>=0]
* Chain [42]: 5*s(682)+1*s(683)+1*s(684)+1*s(686)+1*s(687)+1*s(688)+6
Such that:s(679) =< V1
s(681) =< 2*V1+1
aux(121) =< V1+1
s(688) =< aux(121)
s(682) =< s(679)
s(683) =< aux(121)
s(684) =< s(681)
s(682) =< s(681)
s(683) =< s(681)
s(685) =< s(679)-1
s(686) =< s(684)*s(679)
s(687) =< s(682)*s(685)
with precondition: [V4=0,V=Out,V>=0,V1>=1]
* Chain [41]: 2*s(689)+5*s(694)+1*s(695)+1*s(696)+1*s(698)+1*s(699)+6
Such that:s(691) =< V1
s(692) =< V1+1
s(693) =< 2*V1+1
aux(122) =< V
s(689) =< aux(122)
s(694) =< s(691)
s(695) =< s(692)
s(696) =< s(693)
s(694) =< s(693)
s(695) =< s(693)
s(697) =< s(691)-1
s(698) =< s(696)*s(691)
s(699) =< s(694)*s(697)
with precondition: [V4=0,V1=Out,V>=1,V1>=0]
* Chain [40]: 3*s(573)+4*s(574)+10*s(580)+2*s(581)+2*s(582)+2*s(584)+2*s(585)+1*s(597)+6
Such that:aux(104) =< V
aux(105) =< V1
aux(106) =< V1+1
aux(107) =< 2*V1+1
aux(108) =< V4
s(573) =< aux(104)
s(574) =< aux(108)
s(580) =< aux(105)
s(581) =< aux(106)
s(582) =< aux(107)
s(580) =< aux(107)
s(581) =< aux(107)
s(583) =< aux(105)-1
s(584) =< s(582)*aux(105)
s(585) =< s(580)*s(583)
s(597) =< aux(106)
with precondition: [V1=Out,V1>=0,V4>=1,V>=V4+1]
* Chain [39,46]: 50*s(8)+161*s(10)+14
Such that:aux(123) =< 1
aux(124) =< V
s(10) =< aux(123)
s(8) =< aux(124)
with precondition: [V1=0,V4=0,Out=0,V>=1]
* Chain [39,45]: 51*s(434)+20*s(493)+14
Such that:aux(125) =< 1
aux(126) =< V
s(434) =< aux(125)
s(493) =< aux(126)
with precondition: [V1=0,V4=0,V=Out,V>=1]
* Chain [39,40]: 4*s(573)+10*s(574)+13
Such that:aux(127) =< 1
aux(128) =< V
s(574) =< aux(127)
s(573) =< aux(128)
with precondition: [V1=0,V4=0,Out=0,V>=2]
* Chain [38,[37],46]: 6*it(37)+50*s(8)+89*s(10)+22*s(13)+130*s(25)+26*s(26)+26*s(27)+26*s(29)+26*s(30)+1*s(422)+2*s(423)+5*s(424)+1*s(425)+1*s(426)+1*s(427)+1*s(428)+1*s(429)+13
Such that:aux(58) =< 1
aux(130) =< V
aux(131) =< V1
aux(132) =< V1+1
aux(133) =< 2*V1+1
s(8) =< aux(130)
it(37) =< aux(131)
s(13) =< aux(58)
s(10) =< aux(132)
s(25) =< aux(131)
s(26) =< aux(132)
s(27) =< aux(133)
s(25) =< aux(133)
s(26) =< aux(133)
s(28) =< aux(131)-1
s(29) =< s(27)*aux(131)
s(30) =< s(25)*s(28)
aux(69) =< aux(131)*2+1
aux(68) =< aux(131)+1
aux(67) =< aux(131)
s(433) =< it(37)*aux(130)
s(422) =< it(37)*aux(130)
s(430) =< it(37)*aux(69)
s(431) =< it(37)*aux(68)
s(432) =< it(37)*aux(67)
s(429) =< s(431)
s(423) =< s(433)
s(424) =< s(432)
s(425) =< s(431)
s(426) =< s(430)
s(424) =< s(430)
s(425) =< s(430)
s(427) =< s(426)*aux(131)
s(428) =< s(424)*s(28)
with precondition: [V4=0,Out=0,V>=2,V1>=1]
* Chain [38,[37],45]: 6*it(37)+1*s(422)+2*s(423)+5*s(424)+1*s(425)+1*s(426)+1*s(427)+1*s(428)+1*s(429)+24*s(434)+7*s(435)+55*s(444)+11*s(445)+11*s(446)+11*s(448)+11*s(449)+20*s(493)+13
Such that:aux(93) =< 1
aux(134) =< V1
aux(135) =< V1+1
aux(136) =< 2*V1+1
aux(137) =< Out
it(37) =< aux(134)
s(493) =< aux(137)
s(435) =< aux(93)
s(434) =< aux(135)
s(444) =< aux(134)
s(445) =< aux(135)
s(446) =< aux(136)
s(444) =< aux(136)
s(445) =< aux(136)
s(419) =< aux(134)-1
s(448) =< s(446)*aux(134)
s(449) =< s(444)*s(419)
aux(69) =< aux(134)*2+1
aux(68) =< aux(134)+1
aux(67) =< aux(134)
s(433) =< it(37)*aux(137)
s(422) =< it(37)*aux(137)
s(430) =< it(37)*aux(69)
s(431) =< it(37)*aux(68)
s(432) =< it(37)*aux(67)
s(429) =< s(431)
s(423) =< s(433)
s(424) =< s(432)
s(425) =< s(431)
s(426) =< s(430)
s(424) =< s(430)
s(425) =< s(430)
s(427) =< s(426)*aux(134)
s(428) =< s(424)*s(419)
with precondition: [V4=0,V=Out,V>=2,V1>=1]
* Chain [38,[37],40]: 14*it(37)+1*s(422)+2*s(423)+5*s(424)+1*s(425)+1*s(426)+1*s(427)+1*s(428)+1*s(429)+15*s(580)+3*s(581)+3*s(582)+3*s(584)+3*s(585)+2*s(597)+12
Such that:aux(138) =< V
aux(139) =< Out
aux(140) =< Out+1
aux(141) =< 2*Out+1
it(37) =< aux(138)
s(580) =< aux(139)
s(581) =< aux(140)
s(582) =< aux(141)
s(580) =< aux(141)
s(581) =< aux(141)
s(419) =< aux(139)-1
s(584) =< s(582)*aux(139)
s(585) =< s(580)*s(419)
s(597) =< aux(140)
aux(69) =< aux(139)*2+1
aux(68) =< aux(139)+1
aux(67) =< aux(139)
s(433) =< it(37)*aux(138)
s(422) =< it(37)*aux(138)
s(430) =< it(37)*aux(69)
s(431) =< it(37)*aux(68)
s(432) =< it(37)*aux(67)
s(429) =< s(431)
s(423) =< s(433)
s(424) =< s(432)
s(425) =< s(431)
s(426) =< s(430)
s(424) =< s(430)
s(425) =< s(430)
s(427) =< s(426)*aux(139)
s(428) =< s(424)*s(419)
with precondition: [V4=0,V1=Out,V>=3,V1>=1]
* Chain [38,46]: 50*s(8)+95*s(10)+130*s(25)+26*s(26)+26*s(27)+26*s(29)+26*s(30)+16*s(50)+13
Such that:aux(142) =< 1
aux(143) =< V
aux(144) =< V1
aux(145) =< V1+1
aux(146) =< 2*V1+1
s(8) =< aux(143)
s(10) =< aux(142)
s(25) =< aux(144)
s(26) =< aux(145)
s(27) =< aux(146)
s(25) =< aux(146)
s(26) =< aux(146)
s(28) =< aux(144)-1
s(29) =< s(27)*aux(144)
s(30) =< s(25)*s(28)
s(50) =< aux(145)
with precondition: [V4=0,Out=0,V>=1,V1>=1]
* Chain [38,45]: 24*s(434)+55*s(444)+11*s(445)+11*s(446)+11*s(448)+11*s(449)+7*s(469)+20*s(493)+13
Such that:aux(147) =< 1
aux(148) =< V1
aux(149) =< V1+1
aux(150) =< 2*V1+1
aux(151) =< Out
s(493) =< aux(151)
s(434) =< aux(147)
s(444) =< aux(148)
s(445) =< aux(149)
s(446) =< aux(150)
s(444) =< aux(150)
s(445) =< aux(150)
s(447) =< aux(148)-1
s(448) =< s(446)*aux(148)
s(449) =< s(444)*s(447)
s(469) =< aux(149)
with precondition: [V4=0,V=Out,V>=1,V1>=1]
* Chain [38,40]: 4*s(573)+4*s(574)+15*s(580)+3*s(581)+3*s(582)+3*s(584)+3*s(585)+2*s(597)+12
Such that:aux(108) =< 1
aux(152) =< V
aux(153) =< Out
aux(154) =< Out+1
aux(155) =< 2*Out+1
s(573) =< aux(152)
s(574) =< aux(108)
s(580) =< aux(153)
s(581) =< aux(154)
s(582) =< aux(155)
s(580) =< aux(155)
s(581) =< aux(155)
s(583) =< aux(153)-1
s(584) =< s(582)*aux(153)
s(585) =< s(580)*s(583)
s(597) =< aux(154)
with precondition: [V4=0,V1=Out,V>=2,V1>=1]
#### Cost of chains of start(V,V1,V4,V8,V9):
* Chain [47]: 12*s(1011)+416*s(1018)+1261*s(1019)+630*s(1020)+126*s(1021)+126*s(1022)+126*s(1024)+126*s(1025)+239*s(1026)+6*s(1027)+1*s(1032)+1*s(1036)+2*s(1037)+5*s(1038)+1*s(1039)+1*s(1040)+1*s(1041)+1*s(1042)+94*s(1043)+2*s(1045)+2*s(1049)+4*s(1050)+10*s(1051)+2*s(1052)+2*s(1053)+2*s(1054)+2*s(1055)+6*s(1090)+1*s(1119)+1*s(1123)+2*s(1124)+5*s(1125)+1*s(1126)+1*s(1127)+1*s(1128)+1*s(1129)+570*s(1130)+768*s(1137)+1610*s(1139)+322*s(1140)+322*s(1141)+322*s(1143)+322*s(1144)+26*s(1146)+4*s(1151)+4*s(1155)+8*s(1156)+20*s(1157)+4*s(1158)+4*s(1159)+4*s(1160)+4*s(1161)+2*s(1164)+2*s(1168)+4*s(1169)+10*s(1170)+2*s(1171)+2*s(1172)+2*s(1173)+2*s(1174)+2*s(1272)+2*s(1276)+4*s(1277)+10*s(1278)+2*s(1279)+2*s(1280)+2*s(1281)+2*s(1282)+12*s(1289)+2*s(1323)+2*s(1327)+4*s(1328)+10*s(1329)+2*s(1330)+2*s(1331)+2*s(1332)+2*s(1333)+6*s(1448)+1*s(1477)+1*s(1481)+2*s(1482)+5*s(1483)+1*s(1484)+1*s(1485)+1*s(1486)+1*s(1487)+5*s(1492)+1*s(1493)+1*s(1494)+1*s(1496)+1*s(1497)+15
Such that:s(1490) =< V+1
s(1448) =< V-V4
s(1491) =< 2*V+1
s(1090) =< V4-V9
aux(193) =< 1
aux(194) =< V
aux(195) =< V1
aux(196) =< V1+1
aux(197) =< V1-V4+1
aux(198) =< 2*V1+1
aux(199) =< V4
aux(200) =< V8
aux(201) =< V8+1
aux(202) =< V8-V9
aux(203) =< 2*V8+1
aux(204) =< V9+1
s(1137) =< aux(194)
s(1146) =< aux(195)
s(1289) =< aux(197)
s(1011) =< aux(202)
s(1018) =< aux(199)
s(1019) =< aux(193)
s(1020) =< aux(200)
s(1021) =< aux(201)
s(1022) =< aux(203)
s(1020) =< aux(203)
s(1021) =< aux(203)
s(1023) =< aux(200)-1
s(1024) =< s(1022)*aux(200)
s(1025) =< s(1020)*s(1023)
s(1026) =< aux(201)
s(1027) =< aux(200)
s(1028) =< aux(200)*2+1
s(1029) =< aux(200)+1
s(1030) =< aux(200)
s(1031) =< s(1027)*aux(199)
s(1032) =< s(1027)*aux(199)
s(1033) =< s(1027)*s(1028)
s(1034) =< s(1027)*s(1029)
s(1035) =< s(1027)*s(1030)
s(1036) =< s(1034)
s(1037) =< s(1031)
s(1038) =< s(1035)
s(1039) =< s(1034)
s(1040) =< s(1033)
s(1038) =< s(1033)
s(1039) =< s(1033)
s(1041) =< s(1040)*aux(200)
s(1042) =< s(1038)*s(1023)
s(1043) =< aux(204)
s(1044) =< s(1011)*aux(199)
s(1045) =< s(1011)*aux(199)
s(1046) =< s(1011)*s(1028)
s(1047) =< s(1011)*s(1029)
s(1048) =< s(1011)*s(1030)
s(1049) =< s(1047)
s(1050) =< s(1044)
s(1051) =< s(1048)
s(1052) =< s(1047)
s(1053) =< s(1046)
s(1051) =< s(1046)
s(1052) =< s(1046)
s(1054) =< s(1053)*aux(200)
s(1055) =< s(1051)*s(1023)
s(1130) =< aux(196)
s(1139) =< aux(195)
s(1140) =< aux(196)
s(1141) =< aux(198)
s(1139) =< aux(198)
s(1140) =< aux(198)
s(1142) =< aux(195)-1
s(1143) =< s(1141)*aux(195)
s(1144) =< s(1139)*s(1142)
s(1147) =< aux(195)*2+1
s(1148) =< aux(195)+1
s(1149) =< aux(195)
s(1150) =< s(1146)*aux(194)
s(1151) =< s(1146)*aux(194)
s(1152) =< s(1146)*s(1147)
s(1153) =< s(1146)*s(1148)
s(1154) =< s(1146)*s(1149)
s(1155) =< s(1153)
s(1156) =< s(1150)
s(1157) =< s(1154)
s(1158) =< s(1153)
s(1159) =< s(1152)
s(1157) =< s(1152)
s(1158) =< s(1152)
s(1160) =< s(1159)*aux(195)
s(1161) =< s(1157)*s(1142)
s(1163) =< s(1130)*aux(194)
s(1164) =< s(1130)*aux(194)
s(1165) =< s(1130)*s(1147)
s(1166) =< s(1130)*s(1148)
s(1167) =< s(1130)*s(1149)
s(1168) =< s(1166)
s(1169) =< s(1163)
s(1170) =< s(1167)
s(1171) =< s(1166)
s(1172) =< s(1165)
s(1170) =< s(1165)
s(1171) =< s(1165)
s(1173) =< s(1172)*aux(195)
s(1174) =< s(1170)*s(1142)
s(1271) =< s(1137)*aux(194)
s(1272) =< s(1137)*aux(194)
s(1273) =< s(1137)*s(1147)
s(1274) =< s(1137)*s(1148)
s(1275) =< s(1137)*s(1149)
s(1276) =< s(1274)
s(1277) =< s(1271)
s(1278) =< s(1275)
s(1279) =< s(1274)
s(1280) =< s(1273)
s(1278) =< s(1273)
s(1279) =< s(1273)
s(1281) =< s(1280)*aux(195)
s(1282) =< s(1278)*s(1142)
s(1322) =< s(1289)*aux(194)
s(1323) =< s(1289)*aux(194)
s(1324) =< s(1289)*s(1147)
s(1325) =< s(1289)*s(1148)
s(1326) =< s(1289)*s(1149)
s(1327) =< s(1325)
s(1328) =< s(1322)
s(1329) =< s(1326)
s(1330) =< s(1325)
s(1331) =< s(1324)
s(1329) =< s(1324)
s(1330) =< s(1324)
s(1332) =< s(1331)*aux(195)
s(1333) =< s(1329)*s(1142)
s(1476) =< s(1448)*aux(194)
s(1477) =< s(1448)*aux(194)
s(1478) =< s(1448)*s(1147)
s(1479) =< s(1448)*s(1148)
s(1480) =< s(1448)*s(1149)
s(1481) =< s(1479)
s(1482) =< s(1476)
s(1483) =< s(1480)
s(1484) =< s(1479)
s(1485) =< s(1478)
s(1483) =< s(1478)
s(1484) =< s(1478)
s(1486) =< s(1485)*aux(195)
s(1487) =< s(1483)*s(1142)
s(1492) =< aux(194)
s(1493) =< s(1490)
s(1494) =< s(1491)
s(1492) =< s(1491)
s(1493) =< s(1491)
s(1495) =< aux(194)-1
s(1496) =< s(1494)*aux(194)
s(1497) =< s(1492)*s(1495)
s(1118) =< s(1090)*aux(199)
s(1119) =< s(1090)*aux(199)
s(1120) =< s(1090)*s(1028)
s(1121) =< s(1090)*s(1029)
s(1122) =< s(1090)*s(1030)
s(1123) =< s(1121)
s(1124) =< s(1118)
s(1125) =< s(1122)
s(1126) =< s(1121)
s(1127) =< s(1120)
s(1125) =< s(1120)
s(1126) =< s(1120)
s(1128) =< s(1127)*aux(200)
s(1129) =< s(1125)*s(1023)
with precondition: []
Closed-form bounds of start(V,V1,V4,V8,V9):
-------------------------------------
* Chain [47] with precondition: []
- Upper bound: nat(V)*779+1276+nat(V)*6*nat(V)+nat(V)*12*nat(V1)+nat(V)*6*nat(V1+1)+nat(2*V+1)*nat(V)+nat(V)*6*nat(V1-V4+1)+nat(V)*3*nat(V-V4)+nat(V1)*1648+nat(V1)*20*nat(V)+nat(V1)*40*nat(V1)+nat(V1)*4*nat(V1)*nat(V)+nat(V1)*8*nat(V1)*nat(V1)+nat(V1)*4*nat(V1)*nat(V1+1)+nat(V1)*4*nat(V1)*nat(V1-V4+1)+nat(V1)*20*nat(V1+1)+nat(V1)*322*nat(2*V1+1)+nat(V1)*20*nat(V1-V4+1)+nat(V-V4)*nat(V1)+nat(V1)*2*nat(V-V4)*nat(V1)+nat(V4)*416+nat(V4)*3*nat(V8)+nat(V4)*3*nat(V4-V9)+nat(V4)*6*nat(V8-V9)+nat(V8)*639+nat(V8)*10*nat(V8)+nat(V8)*2*nat(V8)*nat(V8)+nat(V8)*4*nat(V8)*nat(V8-V9)+nat(V8)*126*nat(2*V8+1)+nat(V4-V9)*nat(V8)+nat(V8)*2*nat(V4-V9)*nat(V8)+nat(V8)*20*nat(V8-V9)+nat(nat(V)+ -1)*nat(V)+nat(nat(V1)+ -1)*322*nat(V1)+nat(nat(V1)+ -1)*2*nat(V1)*nat(V)+nat(nat(V1)+ -1)*4*nat(V1)*nat(V1)+nat(nat(V1)+ -1)*2*nat(V1)*nat(V1+1)+nat(nat(V1)+ -1)*2*nat(V1)*nat(V1-V4+1)+nat(V-V4)*nat(nat(V1)+ -1)*nat(V1)+nat(nat(V8)+ -1)*126*nat(V8)+nat(nat(V8)+ -1)*nat(V8)*nat(V8)+nat(nat(V8)+ -1)*2*nat(V8)*nat(V8-V9)+nat(V4-V9)*nat(nat(V8)+ -1)*nat(V8)+nat(V+1)+nat(V1+1)*898+nat(V8+1)*365+nat(V9+1)*94+nat(2*V+1)+nat(2*V1+1)*322+nat(2*V8+1)*126+nat(V1-V4+1)*18+nat(V-V4)*9+nat(V-V4)*9*nat(V1)+nat(V4-V9)*9+nat(V4-V9)*9*nat(V8)+nat(V8-V9)*18
- Complexity: n^3
### Maximum cost of start(V,V1,V4,V8,V9): nat(V)*779+1276+nat(V)*6*nat(V)+nat(V)*12*nat(V1)+nat(V)*6*nat(V1+1)+nat(2*V+1)*nat(V)+nat(V)*6*nat(V1-V4+1)+nat(V)*3*nat(V-V4)+nat(V1)*1648+nat(V1)*20*nat(V)+nat(V1)*40*nat(V1)+nat(V1)*4*nat(V1)*nat(V)+nat(V1)*8*nat(V1)*nat(V1)+nat(V1)*4*nat(V1)*nat(V1+1)+nat(V1)*4*nat(V1)*nat(V1-V4+1)+nat(V1)*20*nat(V1+1)+nat(V1)*322*nat(2*V1+1)+nat(V1)*20*nat(V1-V4+1)+nat(V-V4)*nat(V1)+nat(V1)*2*nat(V-V4)*nat(V1)+nat(V4)*416+nat(V4)*3*nat(V8)+nat(V4)*3*nat(V4-V9)+nat(V4)*6*nat(V8-V9)+nat(V8)*639+nat(V8)*10*nat(V8)+nat(V8)*2*nat(V8)*nat(V8)+nat(V8)*4*nat(V8)*nat(V8-V9)+nat(V8)*126*nat(2*V8+1)+nat(V4-V9)*nat(V8)+nat(V8)*2*nat(V4-V9)*nat(V8)+nat(V8)*20*nat(V8-V9)+nat(nat(V)+ -1)*nat(V)+nat(nat(V1)+ -1)*322*nat(V1)+nat(nat(V1)+ -1)*2*nat(V1)*nat(V)+nat(nat(V1)+ -1)*4*nat(V1)*nat(V1)+nat(nat(V1)+ -1)*2*nat(V1)*nat(V1+1)+nat(nat(V1)+ -1)*2*nat(V1)*nat(V1-V4+1)+nat(V-V4)*nat(nat(V1)+ -1)*nat(V1)+nat(nat(V8)+ -1)*126*nat(V8)+nat(nat(V8)+ -1)*nat(V8)*nat(V8)+nat(nat(V8)+ -1)*2*nat(V8)*nat(V8-V9)+nat(V4-V9)*nat(nat(V8)+ -1)*nat(V8)+nat(V+1)+nat(V1+1)*898+nat(V8+1)*365+nat(V9+1)*94+nat(2*V+1)+nat(2*V1+1)*322+nat(2*V8+1)*126+nat(V1-V4+1)*18+nat(V-V4)*9+nat(V-V4)*9*nat(V1)+nat(V4-V9)*9+nat(V4-V9)*9*nat(V8)+nat(V8-V9)*18
Asymptotic class: n^3
* Total analysis performed in 3603 ms.